(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 3.
The certificate found is represented by the following graph.
Start state: 899
Accept states: [900, 901, 902]
Transitions:
899→900[b_1|0]
899→901[c_1|0]
899→902[a_1|0]
899→899[d_1|0]
899→903[c_1|1]
899→904[a_1|1]
899→907[c_1|2]
903→900[c_1|1]
904→905[c_1|1]
905→906[b_1|1]
905→911[c_1|2]
906→901[a_1|1]
906→903[a_1|1]
906→907[a_1|1]
907→908[b_1|2]
907→912[c_1|3]
908→909[a_1|2]
909→910[b_1|2]
909→913[c_1|3]
910→906[a_1|2]
910→914[a_1|2]
911→906[c_1|2]
912→908[c_1|3]
913→910[c_1|3]
914→915[b_1|2]
914→917[c_1|3]
915→916[c_1|2]
916→901[a_1|2]
916→903[a_1|2]
916→907[a_1|2]
917→915[c_1|3]